(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const i0 Int)
(declare-const i1 Int)
(declare-const i2 Int)
(declare-const v3 Bool)
(declare-const i3 Int)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const i4 Int)
(declare-const v6 Bool)
(declare-const i5 Int)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(assert (or (= 362 0) v6 v13))
(assert (or (< 935 0 i2) (=> (<= 0 0) v5) v11))
(assert (or (< 935 (div i4 935) i2) v13 (= 339 (- i2 66) i4 (abs 788))))
(assert (or (= 362 (- i0 326 (* 459 i1))) (>= i5 (- i0)) v0))
(assert (or (= i2 0) (= i2 0) (< 935 (div i4 935) i2)))
(assert (or v15 (= i2 (- 788)) (not v2)))
(assert (or (xor (=> (= (>= i2 i0 0 0) (>= i2 i0 0 0) (>= i2 i0 0 0) (>= i2 i0 0 (- i0)) v5) v6) v5 (>= 0 823) v8 v12 v9 v13 v13 (< 823 (div i4 788))) v11 v6))
(assert (or (= 339 (- i2 66) i4 (abs 788)) v3 (>= i5 (- i0))))
(assert (or v16 v6 v6))
(assert (or v3 v3 v9))
(assert (or v9 (= 339 0 i4 0) (= 339 0 i4 0)))
(assert (or v0 v0 v11))
(assert (or (= i2 (- 788)) (= i2 (- 788)) (not v2)))
(assert (or (= 339 (- i2 66) i4 (abs 788)) v10 (= i2 (- 788))))
(assert (or (xor (=> (= (>= i2 i0 0 0) (>= i2 i0 0 0) (>= i2 i0 0 (- i0)) (>= i2 i0 0 (- i0)) v5) v6) v5 (>= 0 823) v8 v12 v9 v13 v13 (< 823 (div i4 788))) v10 v3))
(assert (or (= i2 (- 788)) (=> (<= 0 0) v5) (= i2 (- 788))))
(assert (or (= 339 (- i2 66) i4 (abs 788)) (= 339 0 i4 0) (< 935 (div i4 935) i2)))
(assert (or (=> (<= 0 0) v5) v10 (=> (<= 0 0) v5)))
(assert (or (= i2 0) (xor (=> (= (>= i2 i0 0 0) (>= i2 i0 0 0) (>= i2 i0 0 0) (>= i2 i0 0 (- i0)) v5) v6) v5 (>= 0 823) v8 v12 v9 v13 v13 (< 823 (div i4 788))) (= 339 0 i4 0)))
(assert (or v13 (=> v2 v7) (>= i2 i0 0 0)))
(assert (or (>= i5 (- i0)) (= i2 (- 788)) v16))
(assert (or (= i2 (- 788)) (= 362 (- i0 326 (* 459 i1))) (= 339 0 i4 0)))
(check-sat)
